D:Dsys, i:Id. d-world-state(D;i)  Type 

latex

Definitions	t  T, Dsys, d-world-state(D;i), M.state, Action(dec), d-decl(D;i), M.Msg, M(i), Id, source(l), mlnk(m), x:A. B(x)
Lemmas	mlnk wf d, lsrc wf, ma-msg wf, d-decl wf, action wf, d-m wf, ma-st wf, dsys wf, Id wf